\begin{tabbing}
locl($a$) sends [${\it tg}$,$f$\{$A$$\rightarrow$$T$\}($x$)] on link $l$ once
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(subtype\_rel(es{-}vartype(${\it es}$; source($l$); $x$); $A$)\+
\\[0ex]$\wedge$ ($\forall$$e$:es{-}E(${\it es}$). (es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$)) $\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); $T$)))
\\[0ex]c$\wedge$ ($\exists$\=$e$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$))
\\[0ex]c$\wedge$ \=((es{-}val(${\it es}$; $e$) = $f$(es{-}when(${\it es}$; $x$; es{-}sender(${\it es}$; $e$))))\+
\\[0ex]$\wedge$ (es{-}kind(${\it es}$; es{-}sender(${\it es}$; $e$)) = locl($a$))
\\[0ex]$\wedge$ \=($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex](es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$))
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)) = locl($a$))
\\[0ex]$\Rightarrow$ (${\it e'}$ = $e$)))))
\-\-\-\-
\end{tabbing}